half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
conv(0) → cons(nil, 0)
conv(s(x)) → cons(conv(half(s(x))), lastbit(s(x)))
↳ QTRS
↳ Overlay + Local Confluence
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
conv(0) → cons(nil, 0)
conv(s(x)) → cons(conv(half(s(x))), lastbit(s(x)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
conv(0) → cons(nil, 0)
conv(s(x)) → cons(conv(half(s(x))), lastbit(s(x)))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
conv(0)
conv(s(x0))
HALF(s(s(x))) → HALF(x)
CONV(s(x)) → LASTBIT(s(x))
CONV(s(x)) → CONV(half(s(x)))
LASTBIT(s(s(x))) → LASTBIT(x)
CONV(s(x)) → HALF(s(x))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
conv(0) → cons(nil, 0)
conv(s(x)) → cons(conv(half(s(x))), lastbit(s(x)))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
conv(0)
conv(s(x0))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
HALF(s(s(x))) → HALF(x)
CONV(s(x)) → LASTBIT(s(x))
CONV(s(x)) → CONV(half(s(x)))
LASTBIT(s(s(x))) → LASTBIT(x)
CONV(s(x)) → HALF(s(x))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
conv(0) → cons(nil, 0)
conv(s(x)) → cons(conv(half(s(x))), lastbit(s(x)))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
conv(0)
conv(s(x0))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
LASTBIT(s(s(x))) → LASTBIT(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
conv(0) → cons(nil, 0)
conv(s(x)) → cons(conv(half(s(x))), lastbit(s(x)))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
conv(0)
conv(s(x0))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
LASTBIT(s(s(x))) → LASTBIT(x)
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
conv(0)
conv(s(x0))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
conv(0)
conv(s(x0))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
LASTBIT(s(s(x))) → LASTBIT(x)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
HALF(s(s(x))) → HALF(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
conv(0) → cons(nil, 0)
conv(s(x)) → cons(conv(half(s(x))), lastbit(s(x)))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
conv(0)
conv(s(x0))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
HALF(s(s(x))) → HALF(x)
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
conv(0)
conv(s(x0))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
conv(0)
conv(s(x0))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
HALF(s(s(x))) → HALF(x)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
CONV(s(x)) → CONV(half(s(x)))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
conv(0) → cons(nil, 0)
conv(s(x)) → cons(conv(half(s(x))), lastbit(s(x)))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
conv(0)
conv(s(x0))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
CONV(s(x)) → CONV(half(s(x)))
half(s(0)) → 0
half(s(s(x))) → s(half(x))
half(0) → 0
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
conv(0)
conv(s(x0))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
conv(0)
conv(s(x0))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RuleRemovalProof
CONV(s(x)) → CONV(half(s(x)))
half(s(0)) → 0
half(s(s(x))) → s(half(x))
half(0) → 0
half(0)
half(s(0))
half(s(s(x0)))
half(s(0)) → 0
POL(0) = 1
POL(CONV(x1)) = x1
POL(half(x1)) = x1
POL(s(x1)) = 2·x1
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
CONV(s(x)) → CONV(half(s(x)))
half(s(s(x))) → s(half(x))
half(0) → 0
half(0)
half(s(0))
half(s(s(x0)))
half(s(s(x))) → s(half(x))
POL(0) = 0
POL(CONV(x1)) = 2·x1
POL(half(x1)) = x1
POL(s(x1)) = 1 + x1
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ DependencyGraphProof
CONV(s(x)) → CONV(half(s(x)))
half(0) → 0
half(0)
half(s(0))
half(s(s(x0)))